Nuprl Lemma : es-real_wf 0,22

P:(ES{i}Prop{i'}). es-real{i:l}(es.P(es))  Type{i''} 
latex


Definitionsx:AB(x), Prop, t  T, es.P(es), x(s), x:AB(x), xt(x)
Lemmases realizer wf, R-realizes wf, event system wf

origin